ds:x:Id fp Type, da:k:Knd fp Type, x, T:Top, ks:Top List, a:Top, snd:msg-spec(ds;da), j:Id.
R-has-loc(ecl-machine3(ds;da;x;T;ks;a;snd);j)
~
if null(ks)
if reduce(l,b. null(ecl-tags(l;snd))  source(l) = j
if  b;false;remove-repeats(IdLnkDeq;msg-spec-links(snd)))
else reduce(l,b. source(l) = j  b;false;remove-repeats(IdLnkDeq;msg-spec-links(snd))) fi 

latex

Definitions	, t  T, x:A. B(x), Top, nil, Prop, b, Type, A, b, x:AB(x), P  Q, x:AB(x), P & Q, P  Q, Unit, left+right, Void, x:A. B(x), Id, S  T, ecl-tags(l;snd), p  q, <a,b>, {T}, SQType(T), s ~ t, x. t(x), ecl-machine3(ds;da;x;T;ks;a;snd), a:A fp B(a), Knd, msg-spec(ds;da), null(as), msg-spec-links(snd), IdLnkDeq, remove-repeats(eq;L), IdLnk, type List, s = t
Lemmas	msg-spec wf, Knd wf, fpf wf, remove-repeats wf, idlnk-deq wf, msg-spec-links wf, Rall-has-loc, IdLnk wf, bool sq, R-lnk-tags-loc, ecl-tags wf, Id wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of null, bnot wf, not wf, assert wf, top wf, null wf3, bool wf